i:Id, ds:x:Id fp Type, x:Id, k:Knd, T:Type, test:(State(ds)T).
((x  dom(ds)))  (R-base-recognize(i;ds;x;k;T;test)  Realizer) 

latex

Definitions	, {T}, SQType(T), P & Q, f || g, State(ds), Top, x. t(x), DeclaredType(ds;x), R-base-recognize(i;ds;x;k;T;test), t  T, P  Q, x:A. B(x), False, P  Q, A, x(s), State(ds)
Lemmas	fpf-single wf, Id sq, fpf-single-dom, fpf-sub-join-right, ma-state-subtype, fpf wf, Knd wf, fpf-trivial-subtype-top, id-deq wf, Id wf, fpf-dom wf, assert wf, not wf, decl-state wf, top wf, fpf-cap wf, fpf-cap-single-join, btrue wf, decl-type wf, ifthenelse wf, fpf-single wf3, fpf-join wf, Reffect wf, Rframe wf, rationals wf, bfalse wf, bool wf, Rinit wf, Rplus wf